Nuprl Lemma : rng_car_wf
11,40
postcript
pdf
r
:rng_sig{i:l}. rng_car(
r
)
Type
latex
Definitions
t
.1
,
rng_car(
r
)
,
t
T
,
x
:
A
.
B
(
x
)
,
rng_sig{i:l}
Lemmas
rng
sig
wf
origin
r:rng_sig{i:l}. rng_car(r) 
Type r:rng_sig{i:l}. rng_car(r) Type Tx:A. B(x)